
%\newcommand{\aletter}[2]{\scriptsize{\left<{\tt #1}, #2\right>}}

\begin{figure}
\begin{minipage}{0.5\textwidth}
\begin{center}
\begin{tikzpicture}[framed, node distance=2cm, font=\small, 
%state/.style={circle, draw=blue!50,fill=blue!10,thick, minimum size = 13mm}
state/.style={circle,thick,draw=red!80, fill=gray!40,minimum size=5mm}
]


\node [state] (before)        {};
\node [yshift=2mm] at (before.north) {t0\_before};
\node (beforeandpoll) [yshift=-5mm] at (before.south) {};
%
\node [state] (poll)   [below of=before]    {};
\node [xshift=-5mm] at (poll.north west) {t0\_poll};
\node (belowofpoll) [below of=poll] {};
\node (pollandafter) [yshift=-6.5mm] at (belowofpoll.south) {};
%
\node [state] (after)  [below of=belowofpoll]      {};
\node [yshift=-2mm] at (after.south) {t0\_after};

%\node (rightofbefore) [right of=before] {};
\node [state] (waitB0)  [right of=before]      {};
\node [yshift=2mm] at (waitB0.north) {tb1\_before};
\node (waitB0andreadyread) [yshift=-5mm] at (waitB0.south) {};
%
\node [state] (readyread)  [right of=poll]      {};
\node [xshift=6mm] at (readyread.north east) {tb1\_read};
\node (readyreadandsynchread) [yshift=-5mm] at (readyread.south) {};
%
%\node (rightofreadyread) [right of=readyread] {};
\node [state] (readynoread)  [right of=readyread]      {};
\node [xshift=10mm] at (readynoread.north east) {tb1\_largerId};
\node (readynoreadandsynchnoread) [yshift=-5mm] at (readynoread.south) {};
%
\node [state] (synchread)  [below of=readyread]      {};
\node [xshift=8mm] at (synchread.north east) {tb1\_rsynch};
\node (synchreadandsleep) [yshift=-5mm] at (synchread.south) {};
%
\node [state] (synchnoread)  [below of=readynoread]      {};
\node [xshift=11mm] at (synchnoread.north east) {tb1\_largerSynch};
%
\node [state] (sleep)  [right of=after]      {};
\node [yshift=-2mm] at (sleep.south) {tb1\_after};

\path[->, very thick]  (before) edge (poll) 
                       (poll) edge (after) 
%
                       (waitB0) edge  (readyread) 
                       (waitB0) edge [bend left] (readynoread) 
                       (readyread) edge (synchread)
                       (readynoread) edge (synchnoread)
                       (synchread) edge  (sleep)
                       (synchnoread) edge [bend left] (sleep);
%
\path[<->, dotted,very thick]  (beforeandpoll) edge node [above] {binary} (waitB0andreadyread) ;
\path[<->, dotted,very thick]  (readyreadandsynchread) edge node [above] {synch} (readynoreadandsynchnoread) ;
\path[<->, dotted,very thick]  (pollandafter) edge node [above] {binary} (synchreadandsleep) ;
\end{tikzpicture}
\end{center}
\end{minipage}
\caption{Model of the lock free barrier of Fig.\ref{code:lfs}. Initially, all leading threads are in ``t0\_before'' and all block 1 threads are in ``tb1\_before''.}
\label{model:lfs}
\end{figure}
